1. $T$ : Type
\\[0ex]2. $n$ : $\mathbb{Z}$
\\[0ex]3. 0 $<$ $n$
\\[0ex]4. $\forall$$x$:$T$, $L$:($T$ List). ($x$ $\in$ nth\_tl($n$ {-} 1;$L$)) $\Rightarrow$ ($x$ $\in$ $L$)
\\[0ex]5. $T$
\\[0ex]6. $T$ List
\\[0ex]7. $n_{1}$ : $\mathbb{Z}$
\\[0ex]8. 0 $<$ $n_{1}$
\\[0ex]9. nth\_tl($n_{1}$ {-} 1;[]) = []
\\[0ex]$\vdash$  nth\_tl($n_{1}$;[]) = []